package kodkod.analysis;

import java.io.PrintWriter;
import java.text.DecimalFormat;
import java.text.NumberFormat;
import java.util.*;

import edu.mit.csail.sdg.alloy4whole.AlloyBenchmark;

import kodkod.analysis.*;
import kodkod.analysis.ordering.DefaultOrdering;
import kodkod.ast.*;
import kodkod.ast.operator.*;
import kodkod.engine.fol2sat.Translation;
import kodkod.instance.Bounds;
import kodkod.instance.Tuple;
import kodkod.instance.TupleSet;
import kodkod.util.ints.IntIterator;
import kodkod.util.ints.IntTreeSet;

public class Analyzer {
	
//	public HCVisitor hcVisitor;
	
	public static OverallAnalysis initialAnalysis;
	
	public static Translation translation;
	
	public static PrintWriter logWriter;
	public static final boolean doLog = false;
	
	public long analyzationTime = 0;
	
	public Analyzer(Translation translation) {
		Analyzer.translation = translation;
		
		analyzationTime = System.currentTimeMillis();
		
		initialAnalysis = new OverallAnalysis(translation.formula);
		
		weightHighlyConstraint(translation.formula, 1.0);

//		for (IfExpression e : initialAnalysis.ifExpressions) {
//			weightHighlyConstraint(e.condition(), 1.0);
//			weightHighlyConstraint(e.condition().not(), 1.0);
//		}
//		
//		for (IfIntExpression e : initialAnalysis.ifIntExpressions) {
//			weightHighlyConstraint(e.condition(), 1.0);
//			weightHighlyConstraint(e.condition().not(), 1.0);
//		}
//		
//		for (Comprehension e : initialAnalysis.comprehensions) {
//			weightHighlyConstraint(e.formula(), 1.0);
//			weightHighlyConstraint(e.formula().not(), 1.0);
//		}
		
		analyzationTime = System.currentTimeMillis() - analyzationTime;
	}
	
	public Analyzer(Problem problem) {
		this(problem.translation);
		log(problem.toString());
		log(problem.command.toString());
		log();
	}
	
	public void log() {log("");}
	public void log(String s) {
		if (doLog) {
			if (logWriter == null) logWriter = AlloyBenchmark.getWriter("_analyzer");
			logWriter.println(s);
		}
	}
	public void log(LeafInfo info, double weight, double expressionWeight) {
		if (!doLog || logWriter == null) return;
		StringBuffer buffer = new StringBuffer();
		buffer.append("#Relation: " + info.index + " " + info.leaf.toString());
		NumberFormat format = new DecimalFormat("#0.00000");
		buffer.append(" Weight: " + format.format(weight));
		buffer.append(" Expressionweight: " + format.format(expressionWeight));
		buffer.append(" Product: " + format.format(weight * expressionWeight));
		log(buffer.toString());
		log();
	}
	
	public void incWeight(Relation leaf, double weight) {
		try {
			initialAnalysis.leafInfos.get(leaf).weight += weight;
		} catch (NullPointerException e) {
			e.printStackTrace();
			System.out.println(leaf + " not found");
			System.exit(1);
		}
	}
	
	public double getVariance(LinkedList<LeafInfo> list) {
		double var = 0, avg = 0;
		//average
		for (LeafInfo info : list) avg += info.getWeight();
		avg = avg / list.size();
		//variance
		for (LeafInfo info : list) var += (info.getWeight() - avg) * (info.getWeight() - avg);
		var = var / list.size();
		return var;
	}
	
	public double getVariance(LinkedList<LeafInfo> list1, LinkedList<LeafInfo> list2, LinkedList<LeafInfo> list3) {
		return getVariance(list1) + getVariance(list2) + getVariance(list3);
	}
	
	public ArrayList<ArrayList<Integer>> getThreeGroups() {
		double EPSILON = 0.001;
		
		ArrayList<LeafInfo> nodes = new ArrayList<LeafInfo>(initialAnalysis.leafInfos.values());
		Collections.sort(nodes);
		
		LinkedList<LeafInfo> firstN = new LinkedList<LeafInfo>();
		LinkedList<LeafInfo> middleN = new LinkedList<LeafInfo>();
		LinkedList<LeafInfo> lastN = new LinkedList<LeafInfo>();
		
		middleN.addAll(nodes);
		firstN.addLast(middleN.removeFirst());
		lastN.addFirst(middleN.removeLast());
		
		while (middleN.size() > 0 &&
				firstN.getLast().getWeight() - EPSILON < middleN.getFirst().getWeight() && 
				firstN.getLast().getWeight() + EPSILON > middleN.getFirst().getWeight()) firstN.addLast(middleN.removeFirst());
		
		while (middleN.size() > 0 &&
				lastN.getFirst().getWeight() - EPSILON < middleN.getLast().getWeight() && 
				lastN.getFirst().getWeight() + EPSILON > middleN.getLast().getWeight()) lastN.addFirst(middleN.removeLast());
		
		double oldVar = getVariance(firstN, middleN, lastN);
		
		while (true) {
			if (middleN.size() == 0) break;
			
			firstN.addLast(middleN.removeFirst());
			double firstVar = getVariance(firstN, middleN, lastN);
			middleN.addFirst(firstN.removeLast());
			
			lastN.addFirst(middleN.removeLast());
			double lastVar = getVariance(firstN, middleN, lastN);
			middleN.addLast(lastN.removeFirst());
			
			if (lastVar <= firstVar && lastVar < oldVar) {
				lastN.addFirst(middleN.removeLast());
				oldVar = lastVar;
			} else if (firstVar < lastVar && firstVar < oldVar) {
				firstN.addLast(middleN.removeFirst());
				oldVar = firstVar;
			} else {
				break;
			}
		}
		
		ArrayList<Integer> first = new ArrayList<Integer>(); for (LeafInfo node : firstN) first.add(node.index);
		ArrayList<Integer> middle = new ArrayList<Integer>(); for (LeafInfo node : middleN) middle.add(node.index);
		ArrayList<Integer> last = new ArrayList<Integer>(); for (LeafInfo node : lastN) last.add(node.index);
		
		ArrayList<ArrayList<Integer>> threeGroups = new ArrayList<ArrayList<Integer>>();
		threeGroups.add(first); threeGroups.add(middle); threeGroups.add(last);
		
		return threeGroups;
	}
	
	public ArrayList<Integer> getRelationIdsOrdered() {
		ArrayList<LeafInfo> nodes = new ArrayList<LeafInfo>(initialAnalysis.leafInfos.values());
		Collections.sort(nodes);
		ArrayList<Integer> indices = new ArrayList<Integer>();
		for (LeafInfo node : nodes) indices.add(node.index);
		return indices;
	}
	
	public ArrayList<Double> getRelationWeightsOrdered() {
		ArrayList<LeafInfo> nodes = new ArrayList<LeafInfo>(initialAnalysis.leafInfos.values());
		Collections.sort(nodes);
		ArrayList<Double> weights = new ArrayList<Double>();
		for (LeafInfo node : nodes) weights.add(node.weight);
		return weights;
	}

	final static int SS_BASE_WEIGHT = 1;
	final static int EQ_BASE_WEIGHT = 2;
	final static int CY_BASE_WEIGHT = 2;
	
	private void weightHighlyConstraint(Formula root, double baseweight) {
		FormulaAnalyzer rootAnalyzer = new FormulaAnalyzer(root, false);
		
		HashMap<Formula, Double> hcf = rootAnalyzer.getHighlyConstrainingFormulas();
		ArrayList<Expression> boundedExpressions = rootAnalyzer.getCardinalityBoundedExpressions();
		
		for (Formula formula : hcf.keySet()) {
			double factor = baseweight * hcf.get(formula);
			
			log("");
			log(formula.toString());
						
			if (formula instanceof ComparisonFormula) {
				ComparisonFormula f = (ComparisonFormula)formula;
				
				if (f.op().equals(ExprCompOperator.SUBSET)) {
					if (boundedExpressions.contains(f.left())) continue;
					factor *= SS_BASE_WEIGHT;
				}
				else if (f.op().equals(ExprCompOperator.EQUALS)) {
					factor *= EQ_BASE_WEIGHT;
				}
				
				Leafs left = new Leafs(f.left());
				Leafs right = new Leafs(f.right());
				if (left.size() > 0 && right.size() > 0) {
					distributeWeights(f.left(), factor);
					distributeWeights(f.right(), factor);
				} 
//				else if (left.size() > 1) {
//					distributeWeights(f.left(), factor);
//				} else if (right.size() > 1) {
//					distributeWeights(f.right(), factor);
//				}
			}
			
			else if (formula instanceof QuantifiedFormula) { // add subset-relation from skolemization
				QuantifiedFormula f = (QuantifiedFormula)formula;
				factor *= SS_BASE_WEIGHT;				
				for (Decl decl : f.decls()) {
					if (!translation.skolemRelations.containsKey(decl.variable())) continue;
					if (boundedExpressions.contains(decl.variable())) continue;
					
					Relation skolemRelation = translation.skolemRelations.get(decl.variable());
					
					incWeight(skolemRelation, factor);
					log(initialAnalysis.leafInfos.get(skolemRelation), factor, 1.0);
					
					distributeWeights(decl.expression(), factor);
				}
			}
			
			else if (formula instanceof MultiplicityFormula) {
				MultiplicityFormula f = (MultiplicityFormula)formula;
				factor *= CY_BASE_WEIGHT;
				distributeWeights(f.expression(), factor);
			}
			
			else if (formula instanceof IntComparisonFormula) {
				IntComparisonFormula f = (IntComparisonFormula)formula;
				factor *= CY_BASE_WEIGHT;
				
				Casts casts = new Casts(f.left());
				casts.addAll(new Casts(f.right()));
				
				factor /= (double)casts.size();
				
				for (Expression exp : casts) {
					distributeWeights(exp, factor);
				}
				
				for (IfIntExpression exp : casts.ifIntExpressions) {
					weightHighlyConstraint(exp.condition(), 1.0);
				}
			}
		}
	}
	
	public void distributeWeights(Expression expression, double factor) {
		ExpressionAnalyzer expressionAnalyzer = ExpressionAnalyzer.get(expression);
		
		HashMap<Relation, Double> relationDominances = expressionAnalyzer.getRelationDominances();
		for (Relation r : relationDominances.keySet()) {
			incWeight(r, factor * relationDominances.get(r));
			log(initialAnalysis.leafInfos.get(r), factor, relationDominances.get(r));
		}
		
//		HashMap<Comprehension, Double> compDominances = expressionAnalyzer.getComprehensionDominances();
//		for (Comprehension comp : compDominances.keySet()) {
//		for (Comprehension comp : expressionAnalyzer.comprehensions) {
//			weightHighlyConstraint(comp.formula(), factor);//factor * compDominances.get(comp));
//		}
		
//		HashMap<IfExpression, Double> iteDominances = expressionAnalyzer.getIfExpressionDominances();
//		for (IfExpression ite : iteDominances.keySet()) {
		for (IfExpression ite : expressionAnalyzer.ifExpressions) {
			weightHighlyConstraint(ite.condition(), 1.0);//factor * iteDominances.get(ite));
			weightHighlyConstraint(ite.condition().not(), 1.0);//factor * iteDominances.get(ite));
		}
	}
}